feat(NumberTheory/Bernoulli): von Staudt-Clausen theorem by seewoo5 · Pull Request #34906 · leanprover-community/mathlib4

seewoo5 · 2026-02-06T05:55:48Z

Rado's proof ("A New Proof of a Theorem of v. Staudt", JLMS 1935) of von Staudt-Clausen theorem. Initially written by AxiomProver (see commit 97a308e) with further golfs with Claude and Codex.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…n section - Remove unused `Units.val_mk` from simp calls - Convert deprecated `induction'` to `induction` in three lemmas - Fix whitespace: `2*m` → `2 * m`, `2*k` → `2 * k`, `)^(` → `) ^ (` - Fix resulting lines exceeding 100 char limit - Add `set_option linter.style.longFile 1800` for file length Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Simplify several proofs by inlining single-use haves, using pow_succ, removing redundant intermediate steps, and leveraging Finset.sum_filter. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…a proofs Remove `have IH := IH` identity bindings, unwrap redundant `have h1 := ...; exact h1` wrapping, inline single-use omega equalities into pow_succ rewrites, and merge consecutive single-use rewrite steps. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…o callers Merge trivial single-use helper lemmas directly into their sole call sites to reduce declaration count and improve code locality. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Golf 4 verbose proofs by replacing manual have-chains with field_simp/ring, leveraging core_algebraic_identity, and eliminating redundant cast round-trips. Net savings: ~130 lines. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…callers Remove lemmas with 1-2 line proof bodies that are used only once or not at all, inlining their proofs at call sites to reduce indirection. Dead code removed: pIntegral_add, pIntegral_even_term Inlined: geom_sum_of_root_of_unity, generator_pow_card_sub_one_eq_one, pIntegral_neg_pow_div_two, pIntegral_odd_term, power_sum_eq_faulhaber, coprime_add_of_coprime_den, von_staudt_clausen_pos Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…d_rest Replace ~120-line proof with ~15-line proof using by_cases on divisibility, Finset.add_sum_erase for the positive case, and Finset.filter_congr for the negative case. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

github-actions · 2026-02-06T05:57:00Z

PR summary ee3a5404e5

Import changes exceeding 2%

%	File
+25.44%	`Mathlib.NumberTheory.Bernoulli`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.Bernoulli	1639	2056	+417 (+25.44%)

Import changes for all files

Files	Import difference
8 files `Mathlib.NumberTheory.ModularForms.DedekindEta` `Mathlib.NumberTheory.ModularForms.Delta` `Mathlib.NumberTheory.ModularForms.Derivative` `Mathlib.NumberTheory.ModularForms.Discriminant` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion`	6
`Mathlib.NumberTheory.LSeries.HurwitzZetaValues`	78
`Mathlib.NumberTheory.ZetaValues`	79
`Mathlib.NumberTheory.BernoulliPolynomials`	415
`Mathlib.NumberTheory.Bernoulli`	417

Declarations diff

+ bernoulli_add_indicator_den_not_dvd
+ bernoulli_add_indicator_eq_sub
+ choose_two_mul_succ_mul_div_eq
+ den_sum_dvd_prod_den
+ exists_int_sum_pow_add_indicator_eq
+ factorization_succ_le_sub_one
+ faulhaber_sum_div_prime_eq
+ pIntegral
+ pIntegral_bernoulli_even_term
+ pIntegral_bernoulli_one_term
+ pIntegral_choose_mul_pow_div
+ pIntegral_faulhaber_sum
+ pIntegral_mul
+ pIntegral_pow_div
+ prod_one_div_prime_den_coprime
+ sum_one_div_prime_eq_indicator_div_add
+ sum_pow_add_indicator_eq_zero
+ sum_pow_filter_eq_faulhaber
+ vonStaudtIndicator
+ vonStaudtPrimes
+ vonStaudt_clausen
+ vonStaudt_sum_den_not_dvd

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Add missing documentation for `vonStaudtIndicator` and `pIntegral`. Remove unused arguments from `cast_ne_zero_of_mem_filter`, `generator_pow_ne_one`, `sum_units_pow_eq_zero_of_not_dvd`, `den_pow_div_dvd`, `valuation_bound`, `pIntegral_pow_div_factor`, and `pIntegral_T1`, along with their call sites. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Remove unused arguments from pIntegral_T2, pIntegral_case_one, even_term_decomposition_identity, power_sum_indicator_divisible_by_p, divisibility_to_rat_eq, sum_other_primes_coprime_p_pos, and cascading unused arguments in pIntegral_second_term, pIntegral_coeff_term, pIntegral_first_term, and pIntegral_even_term_in_sum. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…ther Move pIntegral_of_int, pIntegral_mul, pIntegral_mul_int, pIntegral_mul_nat, and pIntegral_sub to directly after pIntegral_sum so all basic pIntegral closure properties are co-located. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Remove pIntegral_nat_mul and use pIntegral_int_mul directly at call sites, relying on Lean's automatic ℕ → ℤ coercion. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Merge the single-use von_staudt_clausen_zero lemma directly into the k = 0 case of von_staudt_clausen. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Remove single-use i1_term_forms_eq and replace it with a shorter `convert` + `push_cast` + `field_simp` proof inside pIntegral_i1_term_in_sum. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Inline ~20 single-use helper lemmas into their callers, reducing the file from ~1053 to 884 lines and from ~80 to 60 definitions. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

MichaelStollBayreuth · 2026-04-24T09:27:40Z

+Rado's proof is based on Faulhaber's theorem and induction on $k$.
+-/
+
+namespace bernoulli


Suggested change

namespace bernoulli

namespace Bernoulli

Lower-case namespace names are rare in Mathlib ('namespace [a-z].' occurs 414 times, 'namespace [A-Z].' 13461 times). I don't think there is official guidance regarding this point, but my feeling is that Bernoulli fits better with established patterns.

MichaelStollBayreuth · 2026-04-24T09:29:27Z

+
+/- Over `ZMod p`, the nonzero `l`-th power sum equals the negative indicator of `(p - 1) ∣ l`. -/
+private lemma sum_pow_add_indicator_eq_zero (p l : ℕ) [Fact p.Prime] :
+    (∑ v ∈ Finset.range p with v ≠ 0, (v : ZMod p) ^ l) +


Why not usse v ∈ Ico 1 p?
(Moving this; the line numbers had changed.)

MichaelStollBayreuth · 2026-04-24T09:31:30Z

+private lemma den_sum_dvd_prod_den {ι : Type*} (s : Finset ι) (f : ι → ℚ) :
+    (∑ i ∈ s, f i).den ∣ ∏ i ∈ s, (f i).den := by


This would make sense as an API lemma on rational numbers (so I suggest to make it public and move it to a file dealing with basic properties of rational numbers).
In fact, it would be good to also have

the stronger result with s.lcm (fun i \map (f i).den) on the right,

the corresponding result for products.

MichaelStollBayreuth · 2026-04-24T09:56:48Z

+    rw [Finset.sum_insert has, Finset.prod_insert has]
+    exact (Rat.add_den_dvd _ _).trans (mul_dvd_mul_left _ ih)
+
+private lemma pIntegral_mul (p : ℕ) [Fact p.Prime] (x y : ℚ)


Suggested change

private lemma pIntegral_mul (p : ℕ) [Fact p.Prime] (x y : ℚ)

private lemma pIntegral_mul {p : ℕ} [Fact p.Prime] {x y : ℚ}

hx and hy determine p, x and y.

MichaelStollBayreuth · 2026-04-24T10:25:30Z

+  rw [bernoulli_one]
+  obtain rfl | hp2 := eq_or_ne p 2
+  · have h : ((-1 / 2 : ℚ) * (2 * k) * (2 : ℚ) ^ (2 * k - 1) / (2 * k)) =
+        -(2 : ℤ) ^ (2 * k - 2) := by
+      rw [(by lia : 2 * k - 1 = (2 * k - 2) + 1), pow_succ]; push_cast; field_simp
+    simpa [h] using Int.padicValuation_le_one _ (-(2 : ℤ) ^ (2 * k - 2))
+  · have hk_ne : (2 * k : ℚ) ≠ 0 := by positivity
+    have hrw : (-1 / 2 : ℚ) * (2 * k) * (p : ℚ) ^ (2 * k - 1) / (2 * k) =
+        (-1 : ℤ) * ((p : ℚ) ^ (2 * k - 1) / 2) := by
+      field_simp [hk_ne]; push_cast; ring
+    rw [hrw]
+    exact pIntegral_mul p _ _ (by exact_mod_cast Int.padicValuation_le_one p (-1))
+      (pIntegral_pow_div p 2 (2 * k - 1) two_ne_zero (by
+        rw [Nat.factorization_eq_zero_of_not_dvd (fun h ↦ by
+          have := Nat.le_of_dvd two_pos h; have := (Fact.out : p.Prime).two_le; lia)]
+        exact Nat.zero_le _))


Suggested change

rw [bernoulli_one]

obtain rfl | hp2 := eq_or_ne p 2

· have h : ((-1 / 2 : ℚ) * (2 * k) * (2 : ℚ) ^ (2 * k - 1) / (2 * k)) =

-(2 : ℤ) ^ (2 * k - 2) := by

rw [(by lia : 2 * k - 1 = (2 * k - 2) + 1), pow_succ]; push_cast; field_simp

simpa [h] using Int.padicValuation_le_one _ (-(2 : ℤ) ^ (2 * k - 2))

· have hk_ne : (2 * k : ℚ) ≠ 0 := by positivity

have hrw : (-1 / 2 : ℚ) * (2 * k) * (p : ℚ) ^ (2 * k - 1) / (2 * k) =

(-1 : ℤ) * ((p : ℚ) ^ (2 * k - 1) / 2) := by

field_simp [hk_ne]; push_cast; ring

rw [hrw]

exact pIntegral_mul p _ _ (by exact_mod_cast Int.padicValuation_le_one p (-1))

(pIntegral_pow_div p 2 (2 * k - 1) two_ne_zero (by

rw [Nat.factorization_eq_zero_of_not_dvd (fun h ↦ by

have := Nat.le_of_dvd two_pos h; have := (Fact.out : p.Prime).two_le; lia)]

exact Nat.zero_le _))

field_simp

rw [bernoulli_one]

obtain rfl | hp2 := eq_or_ne p 2

· have h : ((-1 / 2 : ℚ) * (2 : ℚ) ^ (2 * k - 1)) = -(2 : ℤ) ^ (2 * k - 2) := by

rw [(by lia : 2 * k - 1 = (2 * k - 2) + 1), pow_succ]; push_cast; field_simp

simpa [h] using Int.padicValuation_le_one _ (-(2 : ℤ) ^ (2 * k - 2))

· refine pIntegral_mul p _ _ ?_ ?_ <;> rw [pIntegral, Rat.padicValuation_le_one_iff]

· norm_num

simpa [Nat.prime_dvd_prime_iff_eq Fact.out Nat.prime_two]

· simp [show p ≠ 1 from Nat.Prime.ne_one Fact.out]

You'll need to import Mathlib.Tactic.NormNum.GCD for the norm_num to work.

MichaelStollBayreuth · 2026-04-24T10:36:42Z

+  have h : ((2 * k + 1).choose (2 * m) : ℚ) / (2 * k + 1) =
+      ((2 * k).choose (2 * m) : ℚ) / (2 * k - 2 * m + 1) := by
+    have hm_le : 2 * m ≤ 2 * k + 1 := by lia
+    rw [div_eq_div_iff (by norm_cast) (by norm_cast; lia)]
+    conv_rhs => norm_cast; rw [Nat.choose_mul_succ_eq]
+    push_cast [Nat.cast_sub hm_le]; ring
+  rw [mul_comm ((2 * k + 1).choose (2 * m) : ℚ) x, mul_div_assoc,
+      mul_comm ((2 * k).choose (2 * m) : ℚ) x, mul_div_assoc, h]


Suggested change

have h : ((2 * k + 1).choose (2 * m) : ℚ) / (2 * k + 1) =

((2 * k).choose (2 * m) : ℚ) / (2 * k - 2 * m + 1) := by

have hm_le : 2 * m ≤ 2 * k + 1 := by lia

rw [div_eq_div_iff (by norm_cast) (by norm_cast; lia)]

conv_rhs => norm_cast; rw [Nat.choose_mul_succ_eq]

push_cast [Nat.cast_sub hm_le]; ring

rw [mul_comm ((2 * k + 1).choose (2 * m) : ℚ) x, mul_div_assoc,

mul_comm ((2 * k).choose (2 * m) : ℚ) x, mul_div_assoc, h]

rw [div_eq_div_iff (by norm_cast) (by norm_cast; lia), mul_right_comm _ x, mul_right_comm _ x]

refine congrArg (· * x) ?_

rw [show (2 * (k : ℚ) - 2 * (m : ℚ) + 1) = (↑(2 * k + 1 - 2 * m) : ℚ) by norm_cast; lia]

exact_mod_cast Nat.choose_mul_succ_eq (2 * k) (2 * m) |>.symm

MichaelStollBayreuth · 2026-04-24T11:54:06Z

+  have h_denom_rat : (2 * (k : ℚ) - 2 * m + 1) = ((d + 1 : ℕ) : ℚ) := by
+    simp only [hd_def]; push_cast [Nat.cast_sub hkm]; ring
+  rw [h_exp, h_denom_rat, mul_div_assoc]
+  exact pIntegral_mul p _ _ (by exact_mod_cast Int.padicValuation_le_one p ((2 * k).choose (2 * m)))


Suggested change

exact pIntegral_mul p _ _ (by exact_mod_cast Int.padicValuation_le_one p ((2 * k).choose (2 * m)))

exact pIntegral_mul p _ _ (mod_cast Int.padicValuation_le_one p ((2 * k).choose (2 * m)))

MichaelStollBayreuth · 2026-04-24T11:54:41Z

+    (ih : pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / p)) :
+    pIntegral p (bernoulli (2 * m) * ((2 * k + 1).choose (2 * m)) *
+      (p : ℚ) ^ (2 * k - 2 * m) / (2 * k + 1)) := by
+  have hp_ne : (p : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.Prime.ne_zero Fact.out)


Suggested change

have hp_ne : (p : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.Prime.ne_zero Fact.out)

have hp_ne : (p : ℚ) ≠ 0 := mod_cast (Nat.Prime.ne_zero Fact.out)

MichaelStollBayreuth · 2026-04-24T12:04:27Z

+    pIntegral p (((2 * k).choose (2 * m) : ℚ) * (p : ℚ) ^ (2 * k - 2 * m - 1) /
+      (2 * k - 2 * m + 1)) := by


If you prove here
pIntegral p (↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) / (2 * ↑k + 1))
instead, then you can simplify the proof of pIntegral_bernoulli_even_term below (from around line 590). It looks like this is the only place where this lemma is used.

OK, maybe not -- it is used twice in the proof below...

MichaelStollBayreuth · 2026-04-24T12:06:20Z

+  apply (Rat.padicValuation p).map_sub_le
+  · rw [mul_assoc, mul_div_assoc]
+    apply pIntegral_mul _ _ _ ih
+    have hpow_mul : ((2 * k).choose (2 * m) : ℚ) * (p : ℚ) ^ (2 * k - 2 * m) /
+        (2 * k - 2 * m + 1) =
+        (p : ℚ) * (((2 * k).choose (2 * m) : ℚ) * P / (2 * k - 2 * m + 1)) := by
+      rw [hpow]; ring
+    rw [choose_two_mul_succ_mul_div_eq k m _ hm_lt, hpow_mul]
+    exact pIntegral_mul _ _ _ (Int.padicValuation_le_one p p) hcmp
+  · unfold vonStaudtIndicator; split_ifs
+    · simp only [one_mul]; rw [choose_two_mul_succ_mul_div_eq k m _ hm_lt]; exact hcmp
+    · simp only [zero_mul, zero_div, map_zero]; exact bot_le


Suggested change

apply (Rat.padicValuation p).map_sub_le

· rw [mul_assoc, mul_div_assoc]

apply pIntegral_mul _ _ _ ih

have hpow_mul : ((2 * k).choose (2 * m) : ℚ) * (p : ℚ) ^ (2 * k - 2 * m) /

(2 * k - 2 * m + 1) =

(p : ℚ) * (((2 * k).choose (2 * m) : ℚ) * P / (2 * k - 2 * m + 1)) := by

rw [hpow]; ring

rw [choose_two_mul_succ_mul_div_eq k m _ hm_lt, hpow_mul]

exact pIntegral_mul _ _ _ (Int.padicValuation_le_one p p) hcmp

· unfold vonStaudtIndicator; split_ifs

· simp only [one_mul]; rw [choose_two_mul_succ_mul_div_eq k m _ hm_lt]; exact hcmp

· simp only [zero_mul, zero_div, map_zero]; exact bot_le

have H x := choose_two_mul_succ_mul_div_eq k m x hm_lt

apply (Rat.padicValuation p).map_sub_le

· rw [mul_assoc, mul_div_assoc]

apply pIntegral_mul _ _ _ ih

have hpow_mul : ((2 * k).choose (2 * m) : ℚ) * (p : ℚ) ^ (2 * k - 2 * m) /

(2 * k - 2 * m + 1) =

(p : ℚ) * (((2 * k).choose (2 * m) : ℚ) * P / (2 * k - 2 * m + 1)) := by

rw [hpow]; ring

rw [H, hpow_mul]

exact pIntegral_mul _ _ _ (Int.padicValuation_le_one p p) hcmp

· unfold vonStaudtIndicator

split_ifs

· grind

· simp

MichaelStollBayreuth · 2026-04-24T12:08:48Z

+  apply (Rat.padicValuation p).map_sum_le
+  intro i hi


Suggested change

apply (Rat.padicValuation p).map_sum_le

intro i hi

refine (Rat.padicValuation p).map_sum_le fun i hi ↦ ?

MichaelStollBayreuth · 2026-04-24T12:14:25Z

+      (Nat.factorization_le_of_le_pow <| calc 2 * k + 1 = (2 * k + 1).choose 1 := by simp
+        _ ≤ 2 ^ (2 * k) := Nat.choose_succ_le_two_pow _ 1
+        _ ≤ p ^ (2 * k) := Nat.pow_le_pow_left (Fact.out : p.Prime).two_le _)


Suggested change

(Nat.factorization_le_of_le_pow <| calc 2 * k + 1 = (2 * k + 1).choose 1 := by simp

_ ≤ 2 ^ (2 * k) := Nat.choose_succ_le_two_pow _ 1

_ ≤ p ^ (2 * k) := Nat.pow_le_pow_left (Fact.out : p.Prime).two_le _)

(factorization_succ_le_sub_one p (2 * k) (by lia) |>.trans tsub_le_self)

since you have factorization_succ_le_sub_one already...

MichaelStollBayreuth · 2026-04-24T12:18:26Z

+private lemma pIntegral_bernoulli_one_term (k p : ℕ) (hk : k > 0) [Fact p.Prime] :
+    pIntegral p (bernoulli 1 * (2 * k) * (p : ℚ) ^ (2 * k - 1) / (2 * k)) := by


The (I think only) use case is
(Rat.padicValuation p) (bernoulli 1 * ↑(2 * k + 1) * ↑p ^ (2 * k - 1) / (2 * ↑k + 1)) ≤ 1.
So it would make sense to prove that instead. (The proof suggested below works also for this version.)

MichaelStollBayreuth · 2026-04-24T12:22:38Z

+    · simp only [bernoulli_eq_zero_of_odd hodd (by lia),
+        zero_mul, zero_div, map_zero]; exact bot_le


Suggested change

· simp only [bernoulli_eq_zero_of_odd hodd (by lia),

zero_mul, zero_div, map_zero]; exact bot_le

· simp [bernoulli_eq_zero_of_odd hodd (by lia)]

MichaelStollBayreuth · 2026-04-24T12:28:10Z

+      (if (p - 1) ∣ 2 * k then 1 else 0)) : ZMod p) = 0 := by
+    push_cast; exact sum_pow_add_indicator_eq_zero p (2 * k)


Suggested change

(if (p - 1) ∣ 2 * k then 1 else 0)) : ZMod p) = 0 := by

push_cast; exact sum_pow_add_indicator_eq_zero p (2 * k)

(if (p - 1) ∣ 2 * k then 1 else 0)) : ZMod p) = 0 :=

mod_cast sum_pow_add_indicator_eq_zero p (2 * k)

MichaelStollBayreuth · 2026-04-24T12:28:29Z

+  rw [show vonStaudtIndicator (2 * k) p = ((if (p - 1) ∣ 2 * k then (1 : ℤ) else 0) : ℚ) by
+    unfold vonStaudtIndicator; split_ifs <;> simp]


Suggested change

rw [show vonStaudtIndicator (2 * k) p = ((if (p - 1) ∣ 2 * k then (1 : ℤ) else 0) : ℚ) by

unfold vonStaudtIndicator; split_ifs <;> simp]

unfold vonStaudtIndicator

MichaelStollBayreuth · 2026-04-24T12:33:25Z

+        (p : ℚ) ^ (2 * k + 1 - i) / (2 * k + 1)) + p * bernoulli (2 * k) := by
+  have hfilter : (∑ v ∈ Finset.range p with v ≠ 0, (v : ℚ) ^ (2 * k)) =
+      ∑ v ∈ Finset.range p, (v : ℚ) ^ (2 * k) :=
+    Finset.sum_filter_of_ne fun v _ hne ↦ by rintro rfl; exact hne (by simp [(by lia : 2 * k ≠ 0)])


Suggested change

Finset.sum_filter_of_ne fun v _ hne ↦ by rintro rfl; exact hne (by simp [(by lia : 2 * k ≠ 0)])

Finset.sum_filter_of_ne fun v _ hne ↦ ne_zero_pow (by lia) (mod_cast hne)

MichaelStollBayreuth · 2026-04-24T12:37:00Z

+  have hne : (2 * k + 1 : ℚ) ≠ 0 := by positivity
+  rw [hfilter, sum_range_pow, Finset.sum_range_succ]
+  push_cast
+  congr 1
+  rw [Nat.choose_succ_self_right, show 2 * k + 1 - 2 * k = 1 by lia, pow_one]
+  push_cast; field_simp [hne]


Suggested change

have hne : (2 * k + 1 : ℚ) ≠ 0 := by positivity

rw [hfilter, sum_range_pow, Finset.sum_range_succ]

push_cast

congr 1

rw [Nat.choose_succ_self_right, show 2 * k + 1 - 2 * k = 1 by lia, pow_one]

push_cast; field_simp [hne]

rw [hfilter, sum_range_pow, Finset.sum_range_succ, Nat.choose_succ_self_right,

show 2 * k + 1 - 2 * k = 1 by lia]

push_cast

field_simp

MichaelStollBayreuth · 2026-04-24T12:46:11Z

+      (p : ℚ) ^ (2 * k + 1 - i) / (2 * k + 1 : ℚ)) / (p : ℚ) =
+      ∑ i ∈ Finset.range (2 * k), bernoulli i * ((2 * k + 1).choose i : ℚ) *
+        (p : ℚ) ^ (2 * k - i) / (2 * k + 1 : ℚ) := by
+  have hp_ne : (p : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr (Fact.out : p.Prime).ne_zero


Suggested change

have hp_ne : (p : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr (Fact.out : p.Prime).ne_zero

have hp_ne : (p : ℚ) ≠ 0 := mod_cast (Fact.out : p.Prime).ne_zero

etc.; this occurs several times.

MichaelStollBayreuth · 2026-04-24T12:48:54Z

+  rw [hAlg]; congr 1; simpa using faulhaber_sum_div_prime_eq k p
+
+/- For fixed prime `p`, the denominator of `B_{2k} + e_{2k}(p)/p` is not divisible by `p`. -/
+private lemma bernoulli_add_indicator_den_not_dvd (k p : ℕ) (hk : k > 0) [Fact p.Prime] :


Suggested change

private lemma bernoulli_add_indicator_den_not_dvd (k p : ℕ) (hk : k > 0) [Fact p.Prime] :

private lemma not_dvd_den_bernoulli_add_indicator (k p : ℕ) (hk : k > 0) [Fact p.Prime] :

MichaelStollBayreuth · 2026-04-24T12:49:48Z

+    exact Rat.padicValuation_le_one_iff.1 ((Rat.padicValuation p).map_sub_le hT_int hR)
+
+/- Extends the fixed-prime nondivisibility result to the full prime correction sum. -/
+private lemma vonStaudt_sum_den_not_dvd (k p : ℕ) (hk : k > 0) [Fact p.Prime] :


Suggested change

private lemma vonStaudt_sum_den_not_dvd (k p : ℕ) (hk : k > 0) [Fact p.Prime] :

private lemma not_dvd_den_vonStaudt_sum (k p : ℕ) (hk : k > 0) [Fact p.Prime] :

(The lemmas are private, so the names don't matter too much, but it is still good practice to follow the naming convention.)

MichaelStollBayreuth · 2026-04-24T12:53:17Z

+    have hT_int : pIntegral p (T : ℚ) := Int.padicValuation_le_one p T
+    have hR : pIntegral p (∑ i ∈ Finset.range (2 * k),
+        bernoulli i * ((2 * k + 1).choose i) * (p : ℚ) ^ (2 * k - i) / (2 * k + 1)) := by
+      apply pIntegral_faulhaber_sum k p hk
+      intro m hm_pos hm_lt
+      exact Rat.padicValuation_le_one_iff.2 (ih m hm_lt hm_pos)
+    exact Rat.padicValuation_le_one_iff.1 ((Rat.padicValuation p).map_sub_le hT_int hR)


Suggested change

have hT_int : pIntegral p (T : ℚ) := Int.padicValuation_le_one p T

have hR : pIntegral p (∑ i ∈ Finset.range (2 * k),

bernoulli i * ((2 * k + 1).choose i) * (p : ℚ) ^ (2 * k - i) / (2 * k + 1)) := by

apply pIntegral_faulhaber_sum k p hk

intro m hm_pos hm_lt

exact Rat.padicValuation_le_one_iff.2 (ih m hm_lt hm_pos)

exact Rat.padicValuation_le_one_iff.1 ((Rat.padicValuation p).map_sub_le hT_int hR)

have hT_int : pIntegral p T := Int.padicValuation_le_one p T

have hR := pIntegral_faulhaber_sum k p hk fun m hm_pos hm_lt ↦

Rat.padicValuation_le_one_iff.mpr (ih m hm_lt hm_pos)

exact Rat.padicValuation_le_one_iff.mp ((Rat.padicValuation p).map_sub_le hT_int hR)

I'd prefer .mp and .mpr over .1 and .2 for the two directions of a logical equivalence; this is easier to read.

MichaelStollBayreuth · 2026-04-24T13:02:42Z

+    refine ⟨_, Rat.coe_int_num_of_den_eq_one ?_⟩
+    by_contra h
+    obtain ⟨p, hp, hdvd⟩ := ne_one_iff_exists_prime_dvd.mp h
+    exact absurd hdvd (by let : Fact p.Prime := ⟨hp⟩; exact vonStaudt_sum_den_not_dvd k p hk)


Suggested change

exact absurd hdvd (by let : Fact p.Prime := ⟨hp⟩; exact vonStaudt_sum_den_not_dvd k p hk)

exact (let : Fact p.Prime := ⟨hp⟩; vonStaudt_sum_den_not_dvd k p hk) hdvd

seewoo5 and others added 14 commits February 5, 2026 15:46

initial vsc

97a308e

style(NumberTheory/Bernoulli): fix lines exceeding 100 char limit

0c0b428

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

style(NumberTheory/Bernoulli): golf proofs in vonStaudtClausen section

231c7e1

Simplify several proofs by inlining single-use haves, using pow_succ, removing redundant intermediate steps, and leveraging Finset.sum_filter. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

style(NumberTheory/Bernoulli): inline 13 single-use helper lemmas int…

2ee2415

…o callers Merge trivial single-use helper lemmas directly into their sole call sites to reduce declaration count and improve code locality. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

style(NumberTheory/Bernoulli): merge and inline consecutive omega haves

6c004ca

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

style(NumberTheory/Bernoulli): remove unused haves and minor cleanup

f0d4ccd

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

minimize imports

8150f9b

revert some claude moves

0bb93d9

wrap lines in sum_primes_eq_indicator_add_rest

65b06cb

github-actions Bot added large-import Automatically added label for PRs with a significant increase in transitive imports t-number-theory Number theory (also use t-algebra or t-analysis to specialize) labels Feb 6, 2026

seewoo5 and others added 9 commits February 5, 2026 22:23

more wrapping

09b4889

minor

4a14bf6

refactor(NumberTheory/Bernoulli): remove pIntegral_nat_mul

a2b5500

Remove pIntegral_nat_mul and use pIntegral_int_mul directly at call sites, relying on Lean's automatic ℕ → ℤ coercion. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

refactor(NumberTheory/Bernoulli): inline von_staudt_clausen_zero

ef90c66

Merge the single-use von_staudt_clausen_zero lemma directly into the k = 0 case of von_staudt_clausen. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

more golf

a6f9018

refactor(NumberTheory/Bernoulli): inline i1_term_forms_eq

19111c7

Remove single-use i1_term_forms_eq and replace it with a shorter `convert` + `push_cast` + `field_simp` proof inside pIntegral_i1_term_in_sum. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

seewoo5 marked this pull request as draft February 6, 2026 17:14

seewoo5 and others added 3 commits February 7, 2026 21:03

remove unused lemmas & add docstring

d46963a

refactor(NumberTheory/Bernoulli): inline single-use lemmas

5d73b9e

Inline ~20 single-use helper lemmas into their callers, reducing the file from ~1053 to 884 lines and from ~80 to 60 definitions. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

small styling

4c210e9

seewoo5 and others added 5 commits April 21, 2026 14:50

pIntegral as abbrev

64379e7

abbrev vonStaudtPrimes

c349149

change to regular comments

8bd31e5

golf von Staudt-Clausen proofs

2182d33

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Merge branch 'master' into vsc

ddc4561

seewoo5 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 21, 2026

MichaelStollBayreuth reviewed Apr 24, 2026

View reviewed changes

MichaelStollBayreuth added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 24, 2026

		private lemma den_sum_dvd_prod_den {ι : Type*} (s : Finset ι) (f : ι → ℚ) :
		(∑ i ∈ s, f i).den ∣ ∏ i ∈ s, (f i).den := by

	private lemma pIntegral_mul (p : ℕ) [Fact p.Prime] (x y : ℚ)
	private lemma pIntegral_mul {p : ℕ} [Fact p.Prime] {x y : ℚ}

	exact pIntegral_mul p _ _ (by exact_mod_cast Int.padicValuation_le_one p ((2 * k).choose (2 * m)))
	exact pIntegral_mul p _ _ (mod_cast Int.padicValuation_le_one p ((2 * k).choose (2 * m)))

	have hp_ne : (p : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.Prime.ne_zero Fact.out)
	have hp_ne : (p : ℚ) ≠ 0 := mod_cast (Nat.Prime.ne_zero Fact.out)

		pIntegral p (((2 * k).choose (2 * m) : ℚ) * (p : ℚ) ^ (2 * k - 2 * m - 1) /
		(2 * k - 2 * m + 1)) := by

	apply (Rat.padicValuation p).map_sum_le
	intro i hi
	refine (Rat.padicValuation p).map_sum_le fun i hi ↦ ?

		private lemma pIntegral_bernoulli_one_term (k p : ℕ) (hk : k > 0) [Fact p.Prime] :
		pIntegral p (bernoulli 1 * (2 * k) * (p : ℚ) ^ (2 * k - 1) / (2 * k)) := by

		· simp only [bernoulli_eq_zero_of_odd hodd (by lia),
		zero_mul, zero_div, map_zero]; exact bot_le

	· simp only [bernoulli_eq_zero_of_odd hodd (by lia),
	zero_mul, zero_div, map_zero]; exact bot_le
	· simp [bernoulli_eq_zero_of_odd hodd (by lia)]

		(if (p - 1) ∣ 2 * k then 1 else 0)) : ZMod p) = 0 := by
		push_cast; exact sum_pow_add_indicator_eq_zero p (2 * k)

		rw [show vonStaudtIndicator (2 * k) p = ((if (p - 1) ∣ 2 * k then (1 : ℤ) else 0) : ℚ) by
		unfold vonStaudtIndicator; split_ifs <;> simp]

	rw [show vonStaudtIndicator (2 * k) p = ((if (p - 1) ∣ 2 * k then (1 : ℤ) else 0) : ℚ) by
	unfold vonStaudtIndicator; split_ifs <;> simp]
	unfold vonStaudtIndicator

	Finset.sum_filter_of_ne fun v _ hne ↦ by rintro rfl; exact hne (by simp [(by lia : 2 * k ≠ 0)])
	Finset.sum_filter_of_ne fun v _ hne ↦ ne_zero_pow (by lia) (mod_cast hne)

	have hp_ne : (p : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr (Fact.out : p.Prime).ne_zero
	have hp_ne : (p : ℚ) ≠ 0 := mod_cast (Fact.out : p.Prime).ne_zero

	private lemma bernoulli_add_indicator_den_not_dvd (k p : ℕ) (hk : k > 0) [Fact p.Prime] :
	private lemma not_dvd_den_bernoulli_add_indicator (k p : ℕ) (hk : k > 0) [Fact p.Prime] :

	private lemma vonStaudt_sum_den_not_dvd (k p : ℕ) (hk : k > 0) [Fact p.Prime] :
	private lemma not_dvd_den_vonStaudt_sum (k p : ℕ) (hk : k > 0) [Fact p.Prime] :

	exact absurd hdvd (by let : Fact p.Prime := ⟨hp⟩; exact vonStaudt_sum_den_not_dvd k p hk)
	exact (let : Fact p.Prime := ⟨hp⟩; vonStaudt_sum_den_not_dvd k p hk) hdvd

Conversation

seewoo5 commented Feb 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Feb 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary ee3a5404e5

Import changes for modified files

Declarations diff

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

MichaelStollBayreuth Apr 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

MichaelStollBayreuth Apr 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

MichaelStollBayreuth Apr 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

MichaelStollBayreuth Apr 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

MichaelStollBayreuth Apr 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

seewoo5 commented Feb 6, 2026 •

edited

Loading

github-actions Bot commented Feb 6, 2026 •

edited

Loading

MichaelStollBayreuth Apr 24, 2026 •

edited

Loading

MichaelStollBayreuth Apr 24, 2026 •

edited

Loading

MichaelStollBayreuth Apr 24, 2026 •

edited

Loading

MichaelStollBayreuth Apr 24, 2026 •

edited

Loading

MichaelStollBayreuth Apr 24, 2026 •

edited

Loading